es:ES, e1, e2:E, P:({e:E| loc(e) = loc(e1)  Id & ((first(e)))} ).
(loc(e2) = loc(e1)  Id)  e@loc(e1). ((first(e)))  Dec(P(e))  Dec(e(e1,e2].P(e)) 

latex

Definitions	x:A. B(x), P & Q, , P  Q, x(s), e(e1,e2].P(e), t  T, x. t(x), A, Dec(P), x:A. B(x), A c B, e loc e' , (e <loc e'), P  Q, {T}, P  Q, False
Lemmas	alle-at wf, not wf, assert wf, es-first wf, decidable wf, Id wf, es-loc wf, es-E wf, event system wf, es-le-loc, es-loc-pred, es-locl-iff, es-locl wf, es-le wf, es-causl wf